Nuprl Lemma : qdist_wf
11,40
postcript
pdf
r
,
s
:rationals. qdist(
r
;
s
)
rationals
latex
Definitions
qdist(
r
;
s
)
,
t
T
,
x
:
A
.
B
(
x
)
Lemmas
rationals
wf
,
qsub
wf
,
qabs
wf
origin
r,s:rationals. qdist(r; s) 
rationals r,s:rationals. qdist(r; s) rationals Tx:A. B(x)